Library pedal_triangle

Require Import TrianglesDefs.
Require Import incidence.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Lemma pedal_triangle_ok : ∀ P,
 match pedal_triangle P with
  (A1,B1,C1) ⇒ perp (line P A1) (line pointB pointC) ∧
                perp (line P B1) (line pointA pointC) ∧
                perp (line P C1) (line pointA pointB)
 end.
Proof.
intros.
destruct P.
simpl. repeat split;
field;auto with triangle_hyps.
Qed.

Lemma cevian_triangle_of_orthocenter_is_pedal :
 eq_triangles (cevian_triangle X_4) (pedal_triangle X_4).
Proof.
unfold eq_triangles, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.

Lemma pedal_triangle_of_circumcenter_is_medial :
 eq_triangles medial_triangle (pedal_triangle X_3).
Proof.
unfold eq_triangles, medial_triangle, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.

Lemma pedal_triangle_of_incenter_is_intouch :
 eq_triangles intouch_triangle (pedal_triangle X_1).
Proof.
unfold eq_triangles, medial_triangle, eq_points;simpl;repeat split;field;auto with triangle_hyps.
Qed.

End Triangle.